COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00006 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.turn on "→"
CS206∂(30)MIDTERM EXAMINATION→FALL 1983
.turn off "→"

	This examination is open book and notes.
Write LISP functions or predicates as follows except where something else is
requested.  Either notation may be used.  Equal credit for all problems.
.item←0

	#. %2odds u%1 is the sequence of odd numbered elements of
the list ⊗u.  Likewise %2evens_u%1 is the sequence of even numbered
elements of ⊗u.  Thus  %2odds_%1_(A_B_C_D_E)_=_(A_C_E), and
%2evens_%1(A_B_C_D_E)_=_(B_D).  %2combine[u,v]%1 is the result of
interleaving elements of ⊗u and ⊗v taking one from each in turn starting
with ⊗u and
putting any left over elements at the end.  Thus
%2combine%1[(A_C_E),(B_D)]_=_(A_B_C_D_E).

	#. Consider conditional expressions %2(if_p_a_b)%1, where any of
⊗p, ⊗a and ⊗b may be conditional expressions.  If any ⊗p is ⊗T or ⊗F, 
the expression may be simplified.  Moreover, any occurrence of ⊗p in
⊗a may be replaced by ⊗T and any occurrence of ⊗p in ⊗b may be
replaced by ⊗F.  %2ifsimp_exp%1 is the result of applying these
simlifications to ⊗exp and its subexpressions until they can no
longer be applied.

	#. Prove that for all S-expressions %2x%1 and %2z%1 and atoms %2y%1,

	%2subst[x,y,subst[x,y,z]] = subst[subst[x,y,x],y,z]%1.

%2subst%1, which substitutes the S-expression %2x%1 for each occurrence
of the atom %2y%1 in the S-expression %2z%1 is defined by

	%2subst[x,y,z] ← qif qat z qthen [qif z = y qthen x qelse z]
qelse subst[x,y,qa z].subst[x,y,qd z]%1.

Be sure and indicate the %AF%1 used in the induction.

	#. Prove %2∀u.combine(odds_u,evens_u)_=_u%1, where the functions were
those of problem 1.
Hint: Depending on how you write the functions, you may be able to
use list induction or you may have to use rank induction.
Be sure to state the induction principle used and define both the
rank function (if any) and the %AF%1 used in the induction.
The schema for rank induction is

%2[∀x.[∀y.rank_y_<_rank_x_⊃_%AF%*(y)]_⊃_%AF%*(x)]_⊃_∀x.%AF%*(x)%1.